Nuprl Lemma : map_is_cons
0,22
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
L
:
A
List,
L2
:
B
List,
b
:
B
.
map(
f
;
L
) = (
b
.
L2
)
{
f
(hd(
L
)) =
b
& map(
f
;tl(
L
)) =
L2
}
latex
Definitions
P
&
Q
,
t
T
,
tl(
l
)
,
hd(
l
)
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
map(
f
;
as
)
,
Prop
,
i
<
j
,
if
b
t
else
f
fi
,
firstn(
n
;
as
)
,
Y
,
i
j
,
False
,
||
as
||
,
i
j
,
A
,
A
B
Lemmas
ge
wf
,
tl
wf
,
hd
wf
,
non
neg
length
,
map
length
,
length
wf1
,
map
wf
,
map
is
append
origin
A, B:Type, f:(A
B), L:A List, L2:B List, b:B.
{f(hd(L)) = b & map(f;tl(L)) = L2} A, B:Type, f:(AB), L:A List, L2:B List, b:B.
{f(hd(L)) = b & map(f;tl(L)) = L2} 
T Qx:A. B(x)
j
t else f fi
j
j
AB